\begin{tabbing}
es\_realizer\{i:l\}
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$rec(\=$X$.(Unit + (${\it left}$:$X$ $\times$ $X$) + (${\it loc}$:Id\+
\\[0ex]$\times$ ($T$:Type\{i\}
\\[0ex]$\times$ ($x$:Id
\\[0ex]$\times$ ($T$ + (rationals$\rightarrow$$T$))))) + (${\it loc}$:Id
\\[0ex]$\times$ ($T$:Type\{i\}
\\[0ex]$\times$ ($x$:Id
\\[0ex]$\times$ (Knd List)))) + (${\it lnk}$:IdLnk $\times$ (${\it tag}$:Id $\times$ (Knd List))) + (${\it loc}$:Id
\\[0ex]$\times$ (${\it ds}$:fpf(Id; $x$.Type\{i\})
\\[0ex]$\times$ ${\it knd}$:Knd
\\[0ex]$\times$ $T$:Type\{i\}
\\[0ex]$\times$ ($x$:Id
\\[0ex]$\times$ \=((decl{-}state(${\it ds}$)$\rightarrow$$T$$\rightarrow$decl{-}type\=\{i:l\}\+\+
\\[0ex](${\it ds}$; $x$)) + (decl{-}state(${\it ds}$)$\rightarrow$$T$$\rightarrow$rationals$\rightarrow$
\-\\[0ex]decl{-}type\=\{i:l\}\+
\\[0ex](${\it ds}$; $x$)))))) + (${\it ds}$:fpf(Id; $x$.Type\{i\})
\-\-\\[0ex]$\times$ (${\it knd}$:Knd
\\[0ex]$\times$ $T$:Type\{i\}
\\[0ex]$\times$ $l$:IdLnk
\\[0ex]$\times$ (${\it dt}$:fpf(Id; $x$.Type\{i\})
\\[0ex]$\times$ \=((${\it tg}$:Id\+
\\[0ex]$\times$ (decl{-}state(${\it ds}$)$\rightarrow$$T$$\rightarrow$(decl{-}type\=\{i:l\}\+
\\[0ex](${\it dt}$; ${\it tg}$) List))) List)))) + (${\it loc}$:Id
\-\-\\[0ex]$\times$ (${\it ds}$:fpf(Id; $x$.Type\{i\})
\\[0ex]$\times$ $a$:Id
\\[0ex]$\times$ ($p$:finite{-}prob{-}space
\\[0ex]$\times$ (decl{-}state(${\it ds}$)$\rightarrow\mathbb{B}$)))) + (${\it loc}$:Id $\times$ ($k$:Knd $\times$ (Id List))) + (${\it loc}$:Id
\\[0ex]$\times$ ($k$:Knd
\\[0ex]$\times$ (IdLnk List))) + (${\it loc}$:Id $\times$ ($x$:Id $\times$ (Knd List)))))
\-
\end{tabbing}